SPECIFICATION Spec
\* Add statements after this line.
INVARIANT Invariant
PROPERTY Termination
